\begin{tabbing}
$\vdash$  \=$\forall$$A$:Type, $P$:($A$$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$), $d$:($\forall$$x$:$A$. Dec($\exists$$n$:$\mathbb{N}$. ($\uparrow$($P$($x$,$n$))))), $x$:$A$.\+
\\[0ex]($\uparrow$can{-}apply(mu'($P$);$x$)) $\Leftarrow\!\Rightarrow$ ($\exists$$n$:$\mathbb{N}$. ($\uparrow$($P$($x$,$n$))))
\-
\end{tabbing}